T:Type, X:MaInterface(T), es:ES.
ma-interface-consistent(es;X)
 (e:E. (ma-in-interface(es;X;e))  (ma-interface-val(es;X;e)  (T + Top))) 

latex

Definitions

x  dom(f), IdDeq, s = t, {x:A| B(x)} , Knd, b, hasloc(k;i), kind(e), loc(e), ma-in-interface(es;X;e), ma-interface-consistent(es;X), MaInterface(T), ma-interface-val(es;X;e), P  Q, P & Q, , A, x.A(x), f(a), KindDeq, (state when e), state@i, val(e), valtype(e), t.2, case b of inl(x) => s(x) | inr(y) => t(y), True, False, IdLnk, b, ff, tt, Unit, , if b then t else f fi , E, t.1, let x,y = A in B(x;y), ES, ma-interface-consistent-at(es;i;X), f(x), P  Q, Id, a:A fp B(a), x. t(x), x:A  B(x), Type, State(ds), x:A. B(x), x:AB(x), left + right, t  T, Top, e@i. P(e), vartype(i;x), f(x)?z, EqDecider(T), strong-subtype(A;B), @i discrete ds, Atom$n, suptype(S; T), S  T, <a, b>, s ~ t, SQType(T), {T}

Lemmas

Knd sq, subtype rel self, subtype rel dep function, es-state-subtype, es-state-subtype2, strong-subtype-self, strong-subtype-set3, strong-subtype-deq-subtype, fpf-cap wf, es-vartype wf, pi1 wf, es-valtype wf, subtype rel wf, alle-at wf, top wf, decl-state wf, hasloc wf, assert wf, fpf wf, fpf-ap wf, es-hasloc, btrue wf, bfalse wf, bnot wf, false wf, true wf, es-kind wf, fpf-trivial-subtype-top, pi2 wf, es-val wf, es-state-when wf, Kind-deq wf, Knd wf, fpf-dom wf, bool wf, Id wf, es-loc wf, id-deq wf, not wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, ma-interface wf, event system wf, ma-interface-consistent wf, es-E wf, ma-in-interface wf